User blog:Syst3ms/A formalization of Pi Notation as an ordinal notation
CRUCIAL : Analysis has shown this version is significantly weaker than Username's intended behaviour past \(\pi(\Omega)\). As such, this version can be considered "incorrect". While it does exhibit noticeable strength, it is extremely tame compared to the intended one. I don't know when I'll continue working on this. Today I am going to propose my formal definition of Username5243's Pi Notation. This notation is infamous for being extremely ill-defined, and even the more-than-informal explanation is confusing. However, I made a little attempt, and while it wasn't any more acceptable than Username's page in terms of an ordinal notation, it was exploitable, and after seeing this blog post by P進大好きbot, I got the idea of trying to finish what i started, and he helped me tremendously with making this post possible. We are going to define an ordinal notation \((OT,[])\) based on a system of fundamental sequences. We are first going to define the base of the ordinal notation with sets of ordinal terms \(T, PT, N\), functions \(\text{rank},\text{co},\text{atom}\) as well as a relation \(<\). From there, we will definethe sets \(\text{Lis},\text{Li},\text{Su},L_\omega\) and the subset \(OT\subset T\) which contains standard forms. We are then going to define the fundamental sequence system using the functions \(F,S\). The expansion rules will rely on the function symbol L as well as two processes. Finally, we will define the fundamental sequence system \(\alphan\). Base of the ordinal notation Ordinal terms Definition of \(T\), the set of all ordinal terms: #\(0 \in T\) #\(a,b \in T : a+b \in T\) #\(a,b,c \in T : \pi_a(b,c) \in T\) #\(a,b \in T : L(a,b) \in T\) Definition of \(PT\), the set of "non-addition" ordinal terms : #\(a,b,c \in T : \pi_a(b,c) \in PT\) #\(a,b \in T : L(a,b) \in PT\) Definition of \(N\), the set of "natural numbers": #\(0,\pi_0(0,0) \in N\) #\(a \in N, a\neq 0 : a+\pi_0(0,0) \in N\) We let \(1\) be a shorthand for \(\pi_0(0,0)\) and \(\omega\) a shorthand for \(\pi_0(0,1)\) Definition of \(\text{rank}(s)\): #\(\text{rank}(0)=0\) #For \(a,b,c\in T\), \(\text{rank}(\pi_a(b,c))=a\) #For \(a\in T,b\in PT\), \(\text{rank}(a+b)=\text{rank}(a)\) #For \(a,b\in T\), \(\text{rank}(L(a,b))=\text{rank}(a)\) Definition of \(\text{co}(s)\), with \(s \in T\) : #\(\text{co}(0)=0\) #If \(s=\pi_a(b,c)\): ##If \(b=0 \wedge c=0\) then \(\text{co}(s)=a\) ##Else if \(\text{co}©\leq a\) then \(\text{co}(s)=\text{co}©\) ##Else if \(\text{co}(b)\leq a\) then \(\text{co}(s)=\text{co}(b)\) ##Otherwise, \(\text{co}(s) = 0\) #If \(s=L(a,b)\) then \(\text{co}(s)=\text{co}(b)\) #Else, \(s=s_1+s_2\) with \(s_1\in PT, s_2 \in T\) then \(\text{co}(s)=\text{co}(s_2)\) Total order \(<\) Definition of the relation \(<\), which is a total order on \(T\): *Let \(s\leq t \iff (s0 \wedge \text{co}(b)\leq n) \implies L(x,y) = \pi_n(a,L(b,y))\) ##\(a=0\): ###\(y=0;b \in \text{Su} \implies L(x,y) = 0\) ###\(b,y \in \text{Su},b=b_1+1;y=y_1+1 \implies L(x,y) = L(x,y_1)+\pi_n(0,b_1)\) ##\(a \in \text{Su},a=a_1+1,a_1 \notin \text{Lis}\): ###\(b,y=0 \implies L(x,y) = 0\) ###\(b\in\text{Su},b=b_1+1;y=0 \implies L(x,y) = \pi_n(a,b_1)+1\) ###\(y\in\text{Su},y=y_1+1\) : ####\(y_1 \notin \text{Lis}\implies L(x,y) = \pi_n(a_1,L(\pi_n(a,b),y_1))\) ####\(y_1 \in \text{Lis}\implies L(x,y) = \pi_n(a_1,L(\pi_n(a,b),y_1)+1)\) ##\(\text{co}(a)=n+1\): ###\(b,y=0 \implies L(x,y) = \pi_n(0,0)\) ###\(b \in \text{Su},b=b_1+1;y=0 \implies L(x,y) = \pi_n(a,b_1)+1\) ###\(y \in \text{Su},y=y_1+1\): ####\(y_1\notin\text{Lis}\implies L(x,y) = \pi_n(L(a,L(\pi_n(a,b),y_1)),0)\) ####\(y_1\in\text{Lis}\implies L(x,y) = \pi_n(L(a,L(\pi_n(a,b),y_1)+1),0)\) ##\(a \in \text{Li}\): ###\(b=0 \implies L(x,y) = \pi_n(L(a,y),0)\) ###\(b \in \text{Su},b=b_1+1 \implies L(x,y) = \pi_n(L(a,y),\pi_n(a,b_1)+1)\) ##\(a \in \text{Su},a=a_1+1,a_1 \in \text{Lis}\): ###\(b,y=0 \implies L(x,y) = 0\) ###\(b\in\text{Su},b=b_1+1;y=0 \implies L(x,y) = \pi_n(a,b_1)+1\) ###\(y\in\text{Su},y=y_1+1 \implies L(x,y) = \pi_n(L(a_1,L(\pi_n(a,b),y_1)),0)\) Definition of \(S(E):T\to OT\) for \(E \in T\), the "standardize" function: #\(S(0) = 0\) #If \(E = L(a,b)\), for \(a,b\in T\): ##\(S(E) = L(S(a),S(b))\) otherwise #If \(E= \pi_n(a,b)\), for \(a,b\in T\): ##If \(S(a)=L(c,\omega)\) then \(S(E)=S(\pi_n(S©,b))\) ##If \(S(b)=L(d,\omega)\) then \(S(E)=S(\pi_n(a,S(d)))\) ##If \(n<\text{co}(S(b))\) then \(S(E) = S(b)\) ##If \(\text{co}(a)=m+1\wedge n\(\alphan = F(L(\alpha,n))\). Of course, this is not a full-fledged ordinal notation because of the lack of a proof of a well-ordering. However, if this notation is as strong as preliminary analysis suggests, then there might not be a strong enough OCF usable to prove the well-ordering. The definition states that S is a function from T to OT, however this property is only assumed, not proven. Proofs : I'll be trying to prove some things. Lemma 1 : \(\equiv\) is symmetric Proof : Obvious from the two last cases of the definition. Lemma 2 : \(\equiv\) is transitive when restricted to \(OT\) Proof : When not restricted to OT, there is only one class of counterexamples : if we take any value \(a\in T\), \(L(a,\omega)\) and \(L(L(a,\omega),\omega)\), transitivity is broken. We have \(a\equiv L(a,\omega)\) and \(L(a,\omega)\equiv L(L(a,\omega),\omega)\) but \(a\not\equiv L(L(a,\omega),\omega)\). However, when restricted to \(OT\), \(L(a,\omega)\notin \text{Lis}\) and therefore \(L(L(a,\omega),\omega) \notin OT\) by point 3 of the definition of \(OT\) and by the definition of \(L_\omega\). This concludes the proof. Category:Blog posts